Nuprl Lemma : int_entire_a
12,41
postcript
pdf
a
,
b
:
.
a
0
b
0
a
*
b
0
latex
ProofTree
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
,
A
,
a
b
T
,
P
Q
,
Dec(
P
)
,
Lemmas
nequal
wf
,
decidable
int
equal
,
int
entire
origin
a, b:
. a 
0 
b 0 a * b 0
a, b:. a 0 b 0 a * b 0
T Qx:A. B(x)
A b T 
Q